Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

Q is empty.


QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))

The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))

The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
QDP
              ↳ ATransformationProof

Q DP problem:
The TRS P consists of the following rules:

A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))

The TRS R consists of the following rules:

a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))

The set Q consists of the following terms:

a(f, a(f, a(g, a(g, x0))))

We have to consider all minimal (P,Q,R)-chains.
We have applied the A-Transformation [17] to get from an applicative problem to a standard problem.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ ATransformationProof
QDP
                  ↳ RFCMatchBoundsDPProof

Q DP problem:
The TRS P consists of the following rules:

f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)

The TRS R consists of the following rules:

f(f(g(g(x)))) → g(g(g(f(f(f(x))))))

The set Q consists of the following terms:

f(f(g(g(x0))))

We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)

To find matches we regarded all rules of R and P:

f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

32, 33, 34, 35, 37, 36, 39, 40, 38, 42, 41, 44, 45, 43, 47, 46, 49, 50, 48, 52, 51, 54, 55, 53, 57, 56, 59, 60, 58, 62, 61, 67, 66, 65, 64, 63

Node 32 is start node and node 33 is final node.

Those nodes are connect through the following edges: